FDL - Nuprl Definition : alle-at

Nuprl Definition : alle-at

0,22

e@i. P(e) ==

e:E. loc(e) = i

P(e)

clarification:

alle-at(es;i;e.P(e)) ==

e:es-E(es). es-loc(es; e) = i

P(e)

Definitions x:A. B(x), E, P Q, Id, loc(e)

FDL editor aliases alle-at

Definitions	x:A. B(x), E, P Q, Id, loc(e)
FDL editor aliases	alle-at